\begin{tabbing}
$\forall$${\it es}$:event\_system\{i:l\}, $e_{1}$,$e_{2}$:es{-}E(${\it es}$), $P$:(\=\{\=$e$:es{-}E(${\it es}$)$\mid$ \+\+
\\[0ex](loc($e$) = loc($e_{1}$) $\in$ Id)
\\[0ex]$\wedge$ ($\neg$($\uparrow$es{-}first(${\it es}$; $e$)))\} 
\-\\[0ex]$\rightarrow$prop\{i:l\}).
\-\\[0ex](loc($e_{2}$) = loc($e_{1}$) $\in$ Id) $\Rightarrow$ ($\exists$$e$$\in$($e_{1}$,$e_{2}$].$P$($e$) $\in$ prop\{i:l\})
\end{tabbing}